/**
  Description:
  
  This example is inspired by a real scala class
  (scala/tools/nsc/transform/TailCalls.scala) used in scalac. 
  This should give some credit to the importance of allowing
  verification of oriented pattern matching.
*/

/** Type refinement: For this example it doesn't need to be recursive because 
    the classes (e.g. ClassDef, ValDef, ...) have no fields (singletons).
 */
   
/* constraint (\forall t. t \in TreeNotWithinPattern <--> 
			~( t \in Dom_WithinPattern)) 
*/

/* domain
	      Dom_Expressions = Expr 				   &
	      Dom_WithinPattern = Match  	                   &
	      Dom_Definitions = (ClassDef \Un ValDef \Un LabelDef)       
*/
  
sealed abstract class Tree   

class ClassDef extends Tree
class ValDef extends Tree
class LabelDef extends Tree

sealed abstract class Match extends Tree
class Sequence extends Match
class Alternative extends Match
class Star extends Match
class Bind extends Match

sealed abstract class Expr extends Tree
class Ident extends Expr
class This extends Expr
class Select extends Expr

object Definitions {
  def unapply(t: Tree): Boolean =
    (t : Tree) match {
      case c : ClassDef => true
      case v : ValDef => true
      case l : LabelDef => true
      case _ => false
    }
}

object Expressions {
  def unapply(e: Expr): Boolean = true
}


object WithinPattern {
  def unapply(t : Match): Boolean = true
}

class TailCallElimination {
 
  def super_transform(tree: Tree): Tree = tree
  
 
  def transform(tree: Tree): Tree = 
  /*
    precondition  tree \in TreeNotWithinPattern
    postcondition res \in TreeNotWithinPattern
  */  
    (tree: Tree) match {

       case Definitions() => this.super_transform(tree)
     
       case Expressions() => tree

    }
}

object Main {

  def main(args: Array[String]): Unit =
    new TailCallElimination().transform(new ClassDef())
}